[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification afs-stream
enrich
   afs-base, 
   buffer-inf-conv

with
   

   
   
   functions  . .stream : file-content → buffer-inf;
              getpage : nat × file-content → buffer;
              getbyte : nat × file-content → data;
   predicates  . ~ . : file-heap × file-heap;
   
   
   
   

   

   axioms files-iso
          : ⊦   files0 ~ files1
              ↔ (∀ ino. 
                     (ino ∈ files0 ↔ ino ∈ files1)
                   ∧ (  ino ∈ files0
                      →   files0[ino].size = files1[ino].size ∧ files0[ino].meta = files1[ino].meta ∧ files0[ino].nlink = files1[ino].nlink
                        ∧ files0[ino].content.stream to files0[ino].size = files1[ino].content.stream to files1[ino].size));
          stream :  ⊦ content.stream = ⌜λ n. getbyte(n, content)⌝ ;
          getpage :  ⊦ getpage(n, content) = (n ∈ content ⊃ content[n];zeropage);
          getbyte :  ⊦ getbyte(m, content) = getpage(m / VFS_PAGE_SIZE, content)[m % VFS_PAGE_SIZE];

   

   
end enrich